(DEFPROP SAMEF
 (NIL SAMEFRINGE SAME SAMEFRINGE1 SAME1 SAMEFRINGE2 SAME2 NEXT ABOT SAMEFRINGE3 SAMEFRINGE4 SAME4 DIGATOM)
VALUE)

(DEFPROP SAMEFRINGE
 (LAMBDA (X Y) (OR (AND (NOT (ATOM X)) (NOT (ATOM Y)) (SAME (CAR X) (CAR Y) (CDR X) (CDR Y))) (EQ X Y)))
EXPR)

(DEFPROP SAME
 (LAMBDA(X Y U V)
  (OR (AND (NOT (ATOM X)) (NOT (ATOM Y)) (SAME (CAR X) (CAR Y) (CONS (CDR X) U) (CONS (CDR Y) V)))
      (AND (NOT (ATOM Y)) (SAME X (CAR Y) U (CONS (CDR Y) V)))
      (AND (NOT (ATOM X)) (SAME (CAR X) Y (CONS (CDR X) U) V))
      (AND (EQ X Y) (SAMEFRINGE U V))))
EXPR)

(DEFPROP SAMEFRINGE1
 (LAMBDA (X Y) (OR (EQ X Y) (AND (NOT (ATOM X)) (NOT (ATOM Y)) (SAME1 (CAR X) (CAR Y) (CDR X) (CDR Y)))))
EXPR)

(DEFPROP SAME1
 (LAMBDA(X Y U V)
  (COND	((ATOM X) (COND ((ATOM Y) (AND (EQ X Y) (SAMEFRINGE1 U V))) (T (SAME1 X (CAR Y) U (CONS (CDR Y) V)))))
	((ATOM Y) (SAME1 (CAR X) Y (CONS (CDR X) U) V))
	(T (SAME1 (CAR X) (CAR Y) (CONS (CDR X) U) (CONS (CDR Y) V)))))
EXPR)

(DEFPROP SAMEFRINGE2
 (LAMBDA (X Y) (SAME2 (ABOT (LIST X)) (ABOT (LIST Y))))
EXPR)

(DEFPROP SAME2
 (LAMBDA(U V)
  (OR (AND (NULL U) (NULL V))
      (AND (NOT (NULL U)) (NOT (NULL V)) (EQ (CAR U) (CAR V)) (SAME2 (NEXT U) (NEXT V)))))
EXPR)

(DEFPROP NEXT
 (LAMBDA(U)
  (COND ((NULL U) NIL) ((EQ (CADR U) 'A) (ABOT (CONS (CDADDR U) (CONS 'D (CDDR U))))) (T (NEXT (CDDR U)))))
EXPR)

(DEFPROP ABOT
 (LAMBDA (U) (COND ((ATOM (CAR U)) U) (T (ABOT (CONS (CAAR U) (CONS 'A U))))))
EXPR)

(DEFPROP SAMEFRINGE3
 (LAMBDA(X Y)
  (OR (EQ X Y)
      (AND (NOT (ATOM X))
	   (NOT (ATOM Y))
	   ((LAMBDA (U V) (AND (EQ (CAR U) (CAR V)) (SAMEFRINGE3 (CDR U) (CDR V)))) (DIGATOM X) (DIGATOM Y)))))
EXPR)

(DEFPROP SAMEFRINGE4
 (LAMBDA (X Y) (OR (EQ X Y) (AND (NOT (ATOM X)) (NOT (ATOM Y)) (SAME4 (DIGATOM X) (DIGATOM Y)))))
EXPR)

(DEFPROP SAME4
 (LAMBDA (X Y) (AND (EQ (CAR X) (CAR Y)) (SAMEFRINGE4 (CDR X) (CDR Y))))
EXPR)

(DEFPROP DIGATOM
 (LAMBDA (U) (COND ((ATOM (CAR U)) U) (T (DIGATOM (CONS (CAAR U) (CONS (CDAR U) (CDR U)))))))
EXPR)